(set-logic QF_BV)
(set-info :source |
   Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan: 
   Program analysis as constraint solving. PLDI 2008: 281-292
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun c0 () (_ BitVec 6))
(declare-fun c1 () (_ BitVec 6))
(declare-fun c10 () (_ BitVec 6))
(declare-fun c11 () (_ BitVec 6))
(declare-fun c2 () (_ BitVec 6))
(declare-fun c3 () (_ BitVec 6))
(declare-fun c4 () (_ BitVec 6))
(declare-fun c5 () (_ BitVec 6))
(declare-fun c6 () (_ BitVec 6))
(declare-fun c7 () (_ BitVec 6))
(declare-fun c8 () (_ BitVec 6))
(declare-fun c9 () (_ BitVec 6))
(declare-fun z0_0 () (_ BitVec 6))
(declare-fun z0_1 () (_ BitVec 6))
(declare-fun z0_2 () (_ BitVec 6))
(declare-fun z0_3 () (_ BitVec 6))
(declare-fun z1_0 () (_ BitVec 6))
(declare-fun z1_1 () (_ BitVec 6))
(declare-fun z1_2 () (_ BitVec 6))
(declare-fun z1_3 () (_ BitVec 6))
(declare-fun z10_0 () (_ BitVec 6))
(declare-fun z10_1 () (_ BitVec 6))
(declare-fun z10_2 () (_ BitVec 6))
(declare-fun z10_3 () (_ BitVec 6))
(declare-fun z10_4 () (_ BitVec 6))
(declare-fun z10_5 () (_ BitVec 6))
(declare-fun z11_0 () (_ BitVec 6))
(declare-fun z11_1 () (_ BitVec 6))
(declare-fun z11_2 () (_ BitVec 6))
(declare-fun z11_3 () (_ BitVec 6))
(declare-fun z11_4 () (_ BitVec 6))
(declare-fun z11_5 () (_ BitVec 6))
(declare-fun z12_0 () (_ BitVec 6))
(declare-fun z12_1 () (_ BitVec 6))
(declare-fun z12_2 () (_ BitVec 6))
(declare-fun z12_3 () (_ BitVec 6))
(declare-fun z12_4 () (_ BitVec 6))
(declare-fun z12_5 () (_ BitVec 6))
(declare-fun z13_0 () (_ BitVec 6))
(declare-fun z13_1 () (_ BitVec 6))
(declare-fun z13_2 () (_ BitVec 6))
(declare-fun z13_3 () (_ BitVec 6))
(declare-fun z13_4 () (_ BitVec 6))
(declare-fun z13_5 () (_ BitVec 6))
(declare-fun z14_0 () (_ BitVec 6))
(declare-fun z14_1 () (_ BitVec 6))
(declare-fun z14_2 () (_ BitVec 6))
(declare-fun z14_3 () (_ BitVec 6))
(declare-fun z14_4 () (_ BitVec 6))
(declare-fun z14_5 () (_ BitVec 6))
(declare-fun z15_0 () (_ BitVec 6))
(declare-fun z15_1 () (_ BitVec 6))
(declare-fun z15_2 () (_ BitVec 6))
(declare-fun z15_3 () (_ BitVec 6))
(declare-fun z15_4 () (_ BitVec 6))
(declare-fun z15_5 () (_ BitVec 6))
(declare-fun z16_0 () (_ BitVec 6))
(declare-fun z16_1 () (_ BitVec 6))
(declare-fun z16_2 () (_ BitVec 6))
(declare-fun z16_3 () (_ BitVec 6))
(declare-fun z16_4 () (_ BitVec 6))
(declare-fun z16_5 () (_ BitVec 6))
(declare-fun z17_0 () (_ BitVec 6))
(declare-fun z17_1 () (_ BitVec 6))
(declare-fun z17_2 () (_ BitVec 6))
(declare-fun z17_3 () (_ BitVec 6))
(declare-fun z17_4 () (_ BitVec 6))
(declare-fun z17_5 () (_ BitVec 6))
(declare-fun z18_0 () (_ BitVec 6))
(declare-fun z18_1 () (_ BitVec 6))
(declare-fun z18_2 () (_ BitVec 6))
(declare-fun z18_3 () (_ BitVec 6))
(declare-fun z18_4 () (_ BitVec 6))
(declare-fun z18_5 () (_ BitVec 6))
(declare-fun z19_0 () (_ BitVec 6))
(declare-fun z19_1 () (_ BitVec 6))
(declare-fun z19_2 () (_ BitVec 6))
(declare-fun z19_3 () (_ BitVec 6))
(declare-fun z19_4 () (_ BitVec 6))
(declare-fun z19_5 () (_ BitVec 6))
(declare-fun z2_0 () (_ BitVec 6))
(declare-fun z2_1 () (_ BitVec 6))
(declare-fun z2_2 () (_ BitVec 6))
(declare-fun z2_3 () (_ BitVec 6))
(declare-fun z20_0 () (_ BitVec 6))
(declare-fun z20_1 () (_ BitVec 6))
(declare-fun z20_2 () (_ BitVec 6))
(declare-fun z20_3 () (_ BitVec 6))
(declare-fun z20_4 () (_ BitVec 6))
(declare-fun z20_5 () (_ BitVec 6))
(declare-fun z21_0 () (_ BitVec 6))
(declare-fun z21_1 () (_ BitVec 6))
(declare-fun z21_2 () (_ BitVec 6))
(declare-fun z21_3 () (_ BitVec 6))
(declare-fun z21_4 () (_ BitVec 6))
(declare-fun z21_5 () (_ BitVec 6))
(declare-fun z22_0 () (_ BitVec 6))
(declare-fun z22_1 () (_ BitVec 6))
(declare-fun z22_2 () (_ BitVec 6))
(declare-fun z22_3 () (_ BitVec 6))
(declare-fun z22_4 () (_ BitVec 6))
(declare-fun z22_5 () (_ BitVec 6))
(declare-fun z23_0 () (_ BitVec 6))
(declare-fun z23_1 () (_ BitVec 6))
(declare-fun z23_2 () (_ BitVec 6))
(declare-fun z23_3 () (_ BitVec 6))
(declare-fun z23_4 () (_ BitVec 6))
(declare-fun z23_5 () (_ BitVec 6))
(declare-fun z24_0 () (_ BitVec 6))
(declare-fun z24_1 () (_ BitVec 6))
(declare-fun z24_2 () (_ BitVec 6))
(declare-fun z24_3 () (_ BitVec 6))
(declare-fun z24_4 () (_ BitVec 6))
(declare-fun z24_5 () (_ BitVec 6))
(declare-fun z25_0 () (_ BitVec 6))
(declare-fun z25_1 () (_ BitVec 6))
(declare-fun z25_2 () (_ BitVec 6))
(declare-fun z25_3 () (_ BitVec 6))
(declare-fun z25_4 () (_ BitVec 6))
(declare-fun z25_5 () (_ BitVec 6))
(declare-fun z3_0 () (_ BitVec 6))
(declare-fun z3_1 () (_ BitVec 6))
(declare-fun z3_2 () (_ BitVec 6))
(declare-fun z3_3 () (_ BitVec 6))
(declare-fun z4_0 () (_ BitVec 6))
(declare-fun z4_1 () (_ BitVec 6))
(declare-fun z4_2 () (_ BitVec 6))
(declare-fun z4_3 () (_ BitVec 6))
(declare-fun z5_0 () (_ BitVec 6))
(declare-fun z5_1 () (_ BitVec 6))
(declare-fun z5_2 () (_ BitVec 6))
(declare-fun z5_3 () (_ BitVec 6))
(declare-fun z6_0 () (_ BitVec 6))
(declare-fun z6_1 () (_ BitVec 6))
(declare-fun z6_2 () (_ BitVec 6))
(declare-fun z6_3 () (_ BitVec 6))
(declare-fun z6_4 () (_ BitVec 6))
(declare-fun z6_5 () (_ BitVec 6))
(declare-fun z7_0 () (_ BitVec 6))
(declare-fun z7_1 () (_ BitVec 6))
(declare-fun z7_2 () (_ BitVec 6))
(declare-fun z7_3 () (_ BitVec 6))
(declare-fun z7_4 () (_ BitVec 6))
(declare-fun z7_5 () (_ BitVec 6))
(declare-fun z8_0 () (_ BitVec 6))
(declare-fun z8_1 () (_ BitVec 6))
(declare-fun z8_2 () (_ BitVec 6))
(declare-fun z8_3 () (_ BitVec 6))
(declare-fun z8_4 () (_ BitVec 6))
(declare-fun z8_5 () (_ BitVec 6))
(declare-fun z9_0 () (_ BitVec 6))
(declare-fun z9_1 () (_ BitVec 6))
(declare-fun z9_2 () (_ BitVec 6))
(declare-fun z9_3 () (_ BitVec 6))
(declare-fun z9_4 () (_ BitVec 6))
(declare-fun z9_5 () (_ BitVec 6))
(assert (let ((?v_0 (bvneg z4_0)) (?v_1 (bvneg z5_0)) (?v_3 (bvneg (bvmul c7 z6_4))) (?v_2 (bvneg z6_1)) (?v_5 (bvneg (bvmul c8 z6_4))) (?v_4 (bvmul c9 z6_4)) (?v_7 (bvneg (bvmul c1 z7_4))) (?v_6 (bvneg z7_1)) (?v_9 (bvneg (bvmul c2 z7_4))) (?v_8 (bvmul c3 z7_4)) (?v_12 (bvneg (bvmul c8 z8_4))) (?v_10 (bvneg (bvmul c7 z8_4))) (?v_11 (bvmul c9 z8_4)) (?v_15 (bvneg (bvmul c2 z9_4))) (?v_13 (bvneg (bvmul c1 z9_4))) (?v_14 (bvmul c3 z9_4)) (?v_17 (bvneg (bvmul c7 z10_4))) (?v_16 (bvneg z10_1)) (?v_18 (bvneg (bvmul c9 z10_4))) (?v_20 (bvneg (bvmul c1 z11_4))) (?v_19 (bvneg z11_1)) (?v_21 (bvneg (bvmul c3 z11_4))) (?v_22 (bvneg z12_0)) (?v_23 (bvneg (bvmul c7 z12_4))) (?v_24 (bvneg (bvmul c9 z12_4))) (?v_25 (bvneg z13_0)) (?v_26 (bvneg (bvmul c1 z13_4))) (?v_27 (bvneg (bvmul c3 z13_4))) (?v_28 (bvneg (bvmul c7 z14_4))) (?v_29 (bvneg (bvmul c9 z14_4))) (?v_30 (bvneg (bvmul c1 z15_4))) (?v_31 (bvneg (bvmul c3 z15_4))) (?v_32 (bvneg z16_0)) (?v_33 (bvneg z16_1)) (?v_34 (bvneg (bvmul c8 z16_4))) (?v_35 (bvneg (bvmul c9 z16_4))) (?v_36 (bvneg z17_0)) (?v_37 (bvneg z17_1)) (?v_38 (bvneg (bvmul c2 z17_4))) (?v_39 (bvneg (bvmul c3 z17_4))) (?v_40 (bvneg z18_0)) (?v_41 (bvneg z18_1)) (?v_42 (bvneg z19_0)) (?v_43 (bvneg z19_1)) (?v_44 (bvneg z20_0)) (?v_45 (bvneg z21_0)) (?v_46 (bvneg (bvmul c8 z22_4))) (?v_47 (bvneg (bvmul c9 z22_4))) (?v_48 (bvneg (bvmul c2 z23_4))) (?v_49 (bvneg (bvmul c3 z23_4))) (?v_50 (bvneg z24_0)) (?v_51 (bvneg z25_0))) (and (bvsle (_ bv63 6) c0) (bvsle c0 (_ bv1 6)) (bvsle (_ bv63 6) c1) (bvsle c1 (_ bv1 6)) (bvsle (_ bv63 6) c10) (bvsle c10 (_ bv1 6)) (bvsle (_ bv63 6) c11) (bvsle c11 (_ bv1 6)) (bvsle (_ bv63 6) c2) (bvsle c2 (_ bv1 6)) (bvsle (_ bv63 6) c3) (bvsle c3 (_ bv1 6)) (bvsle (_ bv63 6) c4) (bvsle c4 (_ bv1 6)) (bvsle (_ bv63 6) c5) (bvsle c5 (_ bv1 6)) (bvsle (_ bv63 6) c6) (bvsle c6 (_ bv1 6)) (bvsle (_ bv63 6) c7) (bvsle c7 (_ bv1 6)) (bvsle (_ bv63 6) c8) (bvsle c8 (_ bv1 6)) (bvsle (_ bv63 6) c9) (bvsle c9 (_ bv1 6)) (bvsle (_ bv0 6) z0_0) (bvsle z0_0 (_ bv1 6)) (bvsle (_ bv0 6) z0_1) (bvsle z0_1 (_ bv1 6)) (bvsle (_ bv0 6) z0_2) (bvsle z0_2 (_ bv1 6)) (bvsle (_ bv1 6) z0_3) (bvsle z0_3 (_ bv15 6)) (bvsle (_ bv0 6) z1_0) (bvsle z1_0 (_ bv1 6)) (bvsle (_ bv0 6) z1_1) (bvsle z1_1 (_ bv1 6)) (bvsle (_ bv0 6) z1_2) (bvsle z1_2 (_ bv1 6)) (bvsle (_ bv1 6) z1_3) (bvsle z1_3 (_ bv15 6)) (bvsle (_ bv0 6) z10_0) (bvsle z10_0 (_ bv1 6)) (bvsle (_ bv0 6) z10_1) (bvsle z10_1 (_ bv1 6)) (bvsle (_ bv0 6) z10_2) (bvsle z10_2 (_ bv1 6)) (bvsle (_ bv0 6) z10_3) (bvsle z10_3 (_ bv1 6)) (bvsle (_ bv0 6) z10_4) (bvsle z10_4 (_ bv1 6)) (bvsle (_ bv1 6) z10_5) (bvsle z10_5 (_ bv15 6)) (bvsle (_ bv0 6) z11_0) (bvsle z11_0 (_ bv1 6)) (bvsle (_ bv0 6) z11_1) (bvsle z11_1 (_ bv1 6)) (bvsle (_ bv0 6) z11_2) (bvsle z11_2 (_ bv1 6)) (bvsle (_ bv0 6) z11_3) (bvsle z11_3 (_ bv1 6)) (bvsle (_ bv0 6) z11_4) (bvsle z11_4 (_ bv1 6)) (bvsle (_ bv1 6) z11_5) (bvsle z11_5 (_ bv15 6)) (bvsle (_ bv0 6) z12_0) (bvsle z12_0 (_ bv1 6)) (bvsle (_ bv63 6) z12_1) (bvsle z12_1 (_ bv1 6)) (bvsle (_ bv0 6) z12_2) (bvsle z12_2 (_ bv1 6)) (bvsle (_ bv0 6) z12_3) (bvsle z12_3 (_ bv1 6)) (bvsle (_ bv0 6) z12_4) (bvsle z12_4 (_ bv1 6)) (bvsle (_ bv1 6) z12_5) (bvsle z12_5 (_ bv15 6)) (bvsle (_ bv0 6) z13_0) (bvsle z13_0 (_ bv1 6)) (bvsle (_ bv63 6) z13_1) (bvsle z13_1 (_ bv1 6)) (bvsle (_ bv0 6) z13_2) (bvsle z13_2 (_ bv1 6)) (bvsle (_ bv0 6) z13_3) (bvsle z13_3 (_ bv1 6)) (bvsle (_ bv0 6) z13_4) (bvsle z13_4 (_ bv1 6)) (bvsle (_ bv1 6) z13_5) (bvsle z13_5 (_ bv15 6)) (bvsle (_ bv0 6) z14_0) (bvsle z14_0 (_ bv1 6)) (bvsle (_ bv0 6) z14_1) (bvsle z14_1 (_ bv1 6)) (bvsle (_ bv0 6) z14_2) (bvsle z14_2 (_ bv1 6)) (bvsle (_ bv0 6) z14_3) (bvsle z14_3 (_ bv1 6)) (bvsle (_ bv0 6) z14_4) (bvsle z14_4 (_ bv1 6)) (bvsle (_ bv1 6) z14_5) (bvsle z14_5 (_ bv15 6)) (bvsle (_ bv0 6) z15_0) (bvsle z15_0 (_ bv1 6)) (bvsle (_ bv0 6) z15_1) (bvsle z15_1 (_ bv1 6)) (bvsle (_ bv0 6) z15_2) (bvsle z15_2 (_ bv1 6)) (bvsle (_ bv0 6) z15_3) (bvsle z15_3 (_ bv1 6)) (bvsle (_ bv0 6) z15_4) (bvsle z15_4 (_ bv1 6)) (bvsle (_ bv1 6) z15_5) (bvsle z15_5 (_ bv15 6)) (bvsle (_ bv0 6) z16_0) (bvsle z16_0 (_ bv1 6)) (bvsle (_ bv0 6) z16_1) (bvsle z16_1 (_ bv1 6)) (bvsle (_ bv0 6) z16_2) (bvsle z16_2 (_ bv1 6)) (bvsle (_ bv0 6) z16_3) (bvsle z16_3 (_ bv1 6)) (bvsle (_ bv0 6) z16_4) (bvsle z16_4 (_ bv1 6)) (bvsle (_ bv1 6) z16_5) (bvsle z16_5 (_ bv15 6)) (bvsle (_ bv0 6) z17_0) (bvsle z17_0 (_ bv1 6)) (bvsle (_ bv0 6) z17_1) (bvsle z17_1 (_ bv1 6)) (bvsle (_ bv0 6) z17_2) (bvsle z17_2 (_ bv1 6)) (bvsle (_ bv0 6) z17_3) (bvsle z17_3 (_ bv1 6)) (bvsle (_ bv0 6) z17_4) (bvsle z17_4 (_ bv1 6)) (bvsle (_ bv1 6) z17_5) (bvsle z17_5 (_ bv15 6)) (bvsle (_ bv0 6) z18_0) (bvsle z18_0 (_ bv1 6)) (bvsle (_ bv0 6) z18_1) (bvsle z18_1 (_ bv1 6)) (bvsle (_ bv0 6) z18_2) (bvsle z18_2 (_ bv1 6)) (bvsle (_ bv0 6) z18_3) (bvsle z18_3 (_ bv1 6)) (bvsle (_ bv0 6) z18_4) (bvsle z18_4 (_ bv1 6)) (bvsle (_ bv1 6) z18_5) (bvsle z18_5 (_ bv15 6)) (bvsle (_ bv0 6) z19_0) (bvsle z19_0 (_ bv1 6)) (bvsle (_ bv0 6) z19_1) (bvsle z19_1 (_ bv1 6)) (bvsle (_ bv0 6) z19_2) (bvsle z19_2 (_ bv1 6)) (bvsle (_ bv0 6) z19_3) (bvsle z19_3 (_ bv1 6)) (bvsle (_ bv0 6) z19_4) (bvsle z19_4 (_ bv1 6)) (bvsle (_ bv1 6) z19_5) (bvsle z19_5 (_ bv15 6)) (bvsle (_ bv0 6) z2_0) (bvsle z2_0 (_ bv1 6)) (bvsle (_ bv63 6) z2_1) (bvsle z2_1 (_ bv1 6)) (bvsle (_ bv0 6) z2_2) (bvsle z2_2 (_ bv1 6)) (bvsle (_ bv1 6) z2_3) (bvsle z2_3 (_ bv15 6)) (bvsle (_ bv0 6) z20_0) (bvsle z20_0 (_ bv1 6)) (bvsle (_ bv0 6) z20_1) (bvsle z20_1 (_ bv1 6)) (bvsle (_ bv0 6) z20_2) (bvsle z20_2 (_ bv1 6)) (bvsle (_ bv0 6) z20_3) (bvsle z20_3 (_ bv1 6)) (bvsle (_ bv0 6) z20_4) (bvsle z20_4 (_ bv1 6)) (bvsle (_ bv1 6) z20_5) (bvsle z20_5 (_ bv15 6)) (bvsle (_ bv0 6) z21_0) (bvsle z21_0 (_ bv1 6)) (bvsle (_ bv0 6) z21_1) (bvsle z21_1 (_ bv1 6)) (bvsle (_ bv0 6) z21_2) (bvsle z21_2 (_ bv1 6)) (bvsle (_ bv0 6) z21_3) (bvsle z21_3 (_ bv1 6)) (bvsle (_ bv0 6) z21_4) (bvsle z21_4 (_ bv1 6)) (bvsle (_ bv1 6) z21_5) (bvsle z21_5 (_ bv15 6)) (bvsle (_ bv0 6) z22_0) (bvsle z22_0 (_ bv1 6)) (bvsle (_ bv0 6) z22_1) (bvsle z22_1 (_ bv1 6)) (bvsle (_ bv0 6) z22_2) (bvsle z22_2 (_ bv1 6)) (bvsle (_ bv0 6) z22_3) (bvsle z22_3 (_ bv1 6)) (bvsle (_ bv0 6) z22_4) (bvsle z22_4 (_ bv1 6)) (bvsle (_ bv1 6) z22_5) (bvsle z22_5 (_ bv15 6)) (bvsle (_ bv0 6) z23_0) (bvsle z23_0 (_ bv1 6)) (bvsle (_ bv0 6) z23_1) (bvsle z23_1 (_ bv1 6)) (bvsle (_ bv0 6) z23_2) (bvsle z23_2 (_ bv1 6)) (bvsle (_ bv0 6) z23_3) (bvsle z23_3 (_ bv1 6)) (bvsle (_ bv0 6) z23_4) (bvsle z23_4 (_ bv1 6)) (bvsle (_ bv1 6) z23_5) (bvsle z23_5 (_ bv15 6)) (bvsle (_ bv0 6) z24_0) (bvsle z24_0 (_ bv1 6)) (bvsle (_ bv0 6) z24_1) (bvsle z24_1 (_ bv1 6)) (bvsle (_ bv0 6) z24_2) (bvsle z24_2 (_ bv1 6)) (bvsle (_ bv0 6) z24_3) (bvsle z24_3 (_ bv1 6)) (bvsle (_ bv0 6) z24_4) (bvsle z24_4 (_ bv1 6)) (bvsle (_ bv1 6) z24_5) (bvsle z24_5 (_ bv15 6)) (bvsle (_ bv0 6) z25_0) (bvsle z25_0 (_ bv1 6)) (bvsle (_ bv0 6) z25_1) (bvsle z25_1 (_ bv1 6)) (bvsle (_ bv0 6) z25_2) (bvsle z25_2 (_ bv1 6)) (bvsle (_ bv0 6) z25_3) (bvsle z25_3 (_ bv1 6)) (bvsle (_ bv0 6) z25_4) (bvsle z25_4 (_ bv1 6)) (bvsle (_ bv1 6) z25_5) (bvsle z25_5 (_ bv15 6)) (bvsle (_ bv0 6) z3_0) (bvsle z3_0 (_ bv1 6)) (bvsle (_ bv63 6) z3_1) (bvsle z3_1 (_ bv1 6)) (bvsle (_ bv0 6) z3_2) (bvsle z3_2 (_ bv1 6)) (bvsle (_ bv1 6) z3_3) (bvsle z3_3 (_ bv15 6)) (bvsle (_ bv0 6) z4_0) (bvsle z4_0 (_ bv1 6)) (bvsle (_ bv0 6) z4_1) (bvsle z4_1 (_ bv1 6)) (bvsle (_ bv0 6) z4_2) (bvsle z4_2 (_ bv1 6)) (bvsle (_ bv1 6) z4_3) (bvsle z4_3 (_ bv15 6)) (bvsle (_ bv0 6) z5_0) (bvsle z5_0 (_ bv1 6)) (bvsle (_ bv0 6) z5_1) (bvsle z5_1 (_ bv1 6)) (bvsle (_ bv0 6) z5_2) (bvsle z5_2 (_ bv1 6)) (bvsle (_ bv1 6) z5_3) (bvsle z5_3 (_ bv15 6)) (bvsle (_ bv0 6) z6_0) (bvsle z6_0 (_ bv1 6)) (bvsle (_ bv0 6) z6_1) (bvsle z6_1 (_ bv1 6)) (bvsle (_ bv0 6) z6_2) (bvsle z6_2 (_ bv1 6)) (bvsle (_ bv0 6) z6_3) (bvsle z6_3 (_ bv1 6)) (bvsle (_ bv0 6) z6_4) (bvsle z6_4 (_ bv1 6)) (bvsle (_ bv1 6) z6_5) (bvsle z6_5 (_ bv15 6)) (bvsle (_ bv0 6) z7_0) (bvsle z7_0 (_ bv1 6)) (bvsle (_ bv0 6) z7_1) (bvsle z7_1 (_ bv1 6)) (bvsle (_ bv0 6) z7_2) (bvsle z7_2 (_ bv1 6)) (bvsle (_ bv0 6) z7_3) (bvsle z7_3 (_ bv1 6)) (bvsle (_ bv0 6) z7_4) (bvsle z7_4 (_ bv1 6)) (bvsle (_ bv1 6) z7_5) (bvsle z7_5 (_ bv15 6)) (bvsle (_ bv0 6) z8_0) (bvsle z8_0 (_ bv1 6)) (bvsle (_ bv63 6) z8_1) (bvsle z8_1 (_ bv1 6)) (bvsle (_ bv0 6) z8_2) (bvsle z8_2 (_ bv1 6)) (bvsle (_ bv0 6) z8_3) (bvsle z8_3 (_ bv1 6)) (bvsle (_ bv0 6) z8_4) (bvsle z8_4 (_ bv1 6)) (bvsle (_ bv1 6) z8_5) (bvsle z8_5 (_ bv15 6)) (bvsle (_ bv0 6) z9_0) (bvsle z9_0 (_ bv1 6)) (bvsle (_ bv63 6) z9_1) (bvsle z9_1 (_ bv1 6)) (bvsle (_ bv0 6) z9_2) (bvsle z9_2 (_ bv1 6)) (bvsle (_ bv0 6) z9_3) (bvsle z9_3 (_ bv1 6)) (bvsle (_ bv0 6) z9_4) (bvsle z9_4 (_ bv1 6)) (bvsle (_ bv1 6) z9_5) (bvsle z9_5 (_ bv15 6)) (= (bvadd z0_0 (bvneg (bvmul c10 z0_2))) (_ bv0 6)) (= (bvadd z0_1 (bvneg (bvmul c11 z0_2))) (_ bv0 6)) (= (bvadd (bvneg z0_0) (bvadd (bvneg z0_2) (bvadd (bvneg (bvmul c6 z0_2)) z0_3))) (_ bv0 6)) (= (bvadd z1_0 (bvneg (bvmul c4 z1_2))) (_ bv0 6)) (= (bvadd z1_1 (bvneg (bvmul c5 z1_2))) (_ bv0 6)) (= (bvadd (bvneg z1_0) (bvadd (bvneg z1_2) (bvadd (bvneg (bvmul c0 z1_2)) z1_3))) (_ bv0 6)) (= (bvadd z2_0 (bvneg (bvmul c11 z2_2))) (_ bv0 6)) (= (bvadd (bvneg z2_1) (bvneg (bvmul c10 z2_2))) (_ bv0 6)) (= (bvadd (bvneg z2_0) (bvadd (bvneg z2_2) (bvadd (bvneg (bvmul c6 z2_2)) z2_3))) (_ bv0 6)) (= (bvadd z3_0 (bvneg (bvmul c5 z3_2))) (_ bv0 6)) (= (bvadd (bvneg z3_1) (bvneg (bvmul c4 z3_2))) (_ bv0 6)) (= (bvadd (bvneg z3_0) (bvadd (bvneg z3_2) (bvadd (bvneg (bvmul c0 z3_2)) z3_3))) (_ bv0 6)) (= (bvadd z4_0 (bvadd (bvmul c3 z4_1) (bvmul c9 z4_2))) (_ bv0 6)) (= (bvadd ?v_0 (bvadd (bvmul c2 z4_1) (bvmul c8 z4_2))) (_ bv0 6)) (= (bvadd ?v_0 (bvadd (bvmul c1 z4_1) (bvmul c7 z4_2))) (_ bv0 6)) (= (bvadd (bvmul c4 z4_1) (bvmul c10 z4_2)) (_ bv0 6)) (= (bvadd (bvmul c5 z4_1) (bvmul c11 z4_2)) (_ bv0 6)) (= (bvadd ?v_0 (bvadd (bvmul c0 z4_1) (bvadd (bvmul c6 z4_2) z4_3))) (_ bv0 6)) (= (bvadd ?v_1 (bvadd (bvmul c3 z5_1) (bvmul c9 z5_2))) (_ bv0 6)) (= (bvadd z5_0 (bvadd (bvmul c2 z5_1) (bvmul c8 z5_2))) (_ bv0 6)) (= (bvadd z5_0 (bvadd (bvmul c1 z5_1) (bvmul c7 z5_2))) (_ bv0 6)) (= (bvadd (bvmul c4 z5_1) (bvmul c10 z5_2)) (_ bv0 6)) (= (bvadd (bvmul c5 z5_1) (bvmul c11 z5_2)) (_ bv0 6)) (= (bvadd ?v_1 (bvadd (bvmul c0 z5_1) (bvadd (bvmul c6 z5_2) z5_3))) (_ bv0 6)) (= (bvadd z6_0 (bvadd (bvmul c4 z6_2) (bvadd (bvmul c10 z6_3) (bvneg (bvmul c10 z6_4))))) (_ bv0 6)) (= (bvadd (bvneg z6_0) (bvadd (bvmul c1 z6_2) (bvadd (bvmul c7 z6_3) ?v_3))) (_ bv0 6)) (= (bvadd z6_1 (bvadd (bvmul c5 z6_2) (bvadd (bvmul c11 z6_3) (bvneg (bvmul c11 z6_4))))) (_ bv0 6)) (= (bvadd ?v_2 (bvadd (bvmul c2 z6_2) (bvadd (bvmul c8 z6_3) ?v_5))) (_ bv0 6)) (= (bvadd (bvmul c3 z6_2) (bvadd (bvmul c9 z6_3) (bvneg ?v_4))) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z6_0) (bvadd ?v_2 (bvadd (bvmul c0 z6_2) (bvadd (bvmul c6 z6_3) (bvadd (bvneg z6_4) (bvadd ?v_3 (bvadd (bvmul (_ bv62 6) ?v_4) (bvadd ?v_5 (bvadd (bvneg (bvmul c6 z6_4)) z6_5))))))))) (_ bv0 6)) (= (bvadd z7_0 (bvadd (bvmul c4 z7_2) (bvadd (bvmul c10 z7_3) (bvneg (bvmul c4 z7_4))))) (_ bv0 6)) (= (bvadd (bvneg z7_0) (bvadd (bvmul c1 z7_2) (bvadd (bvmul c7 z7_3) ?v_7))) (_ bv0 6)) (= (bvadd z7_1 (bvadd (bvmul c5 z7_2) (bvadd (bvmul c11 z7_3) (bvneg (bvmul c5 z7_4))))) (_ bv0 6)) (= (bvadd ?v_6 (bvadd (bvmul c2 z7_2) (bvadd (bvmul c8 z7_3) ?v_9))) (_ bv0 6)) (= (bvadd (bvmul c3 z7_2) (bvadd (bvmul c9 z7_3) (bvneg ?v_8))) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z7_0) (bvadd ?v_6 (bvadd (bvmul c0 z7_2) (bvadd (bvmul c6 z7_3) (bvadd (bvneg z7_4) (bvadd ?v_7 (bvadd (bvmul (_ bv62 6) ?v_8) (bvadd ?v_9 (bvadd (bvneg (bvmul c0 z7_4)) z7_5))))))))) (_ bv0 6)) (= (bvadd z8_0 (bvadd (bvmul c5 z8_2) (bvadd (bvmul c11 z8_3) (bvneg (bvmul c11 z8_4))))) (_ bv0 6)) (= (bvadd (bvneg z8_0) (bvadd (bvmul c2 z8_2) (bvadd (bvmul c8 z8_3) ?v_12))) (_ bv0 6)) (= (bvadd (bvneg z8_1) (bvadd (bvmul c4 z8_2) (bvadd (bvmul c10 z8_3) (bvneg (bvmul c10 z8_4))))) (_ bv0 6)) (= (bvadd z8_1 (bvadd (bvmul c1 z8_2) (bvadd (bvmul c7 z8_3) ?v_10))) (_ bv0 6)) (= (bvadd (bvmul c3 z8_2) (bvadd (bvmul c9 z8_3) (bvneg ?v_11))) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z8_0) (bvadd z8_1 (bvadd (bvmul c0 z8_2) (bvadd (bvmul c6 z8_3) (bvadd (bvneg z8_4) (bvadd ?v_10 (bvadd (bvmul (_ bv62 6) ?v_11) (bvadd ?v_12 (bvadd (bvneg (bvmul c6 z8_4)) z8_5))))))))) (_ bv0 6)) (= (bvadd z9_0 (bvadd (bvmul c5 z9_2) (bvadd (bvmul c11 z9_3) (bvneg (bvmul c5 z9_4))))) (_ bv0 6)) (= (bvadd (bvneg z9_0) (bvadd (bvmul c2 z9_2) (bvadd (bvmul c8 z9_3) ?v_15))) (_ bv0 6)) (= (bvadd (bvneg z9_1) (bvadd (bvmul c4 z9_2) (bvadd (bvmul c10 z9_3) (bvneg (bvmul c4 z9_4))))) (_ bv0 6)) (= (bvadd z9_1 (bvadd (bvmul c1 z9_2) (bvadd (bvmul c7 z9_3) ?v_13))) (_ bv0 6)) (= (bvadd (bvmul c3 z9_2) (bvadd (bvmul c9 z9_3) (bvneg ?v_14))) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z9_0) (bvadd z9_1 (bvadd (bvmul c0 z9_2) (bvadd (bvmul c6 z9_3) (bvadd (bvneg z9_4) (bvadd ?v_13 (bvadd (bvmul (_ bv62 6) ?v_14) (bvadd ?v_15 (bvadd (bvneg (bvmul c0 z9_4)) z9_5))))))))) (_ bv0 6)) (= (bvadd z10_0 (bvadd (bvmul c4 z10_2) (bvadd (bvmul c10 z10_3) (bvneg (bvmul c10 z10_4))))) (_ bv0 6)) (= (bvadd (bvneg z10_0) (bvadd (bvmul c1 z10_2) (bvadd (bvmul c7 z10_3) ?v_17))) (_ bv0 6)) (= (bvadd z10_1 (bvadd (bvmul c5 z10_2) (bvadd (bvmul c11 z10_3) (bvneg (bvmul c11 z10_4))))) (_ bv0 6)) (= (bvadd ?v_16 (bvadd (bvmul c2 z10_2) (bvadd (bvmul c8 z10_3) (bvneg (bvmul c8 z10_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z10_2) (bvadd (bvmul c9 z10_3) ?v_18)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z10_0) (bvadd ?v_16 (bvadd (bvmul c0 z10_2) (bvadd (bvmul c6 z10_3) (bvadd (bvneg z10_4) (bvadd ?v_17 (bvadd (bvneg (bvmul c6 z10_4)) (bvadd ?v_18 z10_5)))))))) (_ bv0 6)) (= (bvadd z11_0 (bvadd (bvmul c4 z11_2) (bvadd (bvmul c10 z11_3) (bvneg (bvmul c4 z11_4))))) (_ bv0 6)) (= (bvadd (bvneg z11_0) (bvadd (bvmul c1 z11_2) (bvadd (bvmul c7 z11_3) ?v_20))) (_ bv0 6)) (= (bvadd z11_1 (bvadd (bvmul c5 z11_2) (bvadd (bvmul c11 z11_3) (bvneg (bvmul c5 z11_4))))) (_ bv0 6)) (= (bvadd ?v_19 (bvadd (bvmul c2 z11_2) (bvadd (bvmul c8 z11_3) (bvneg (bvmul c2 z11_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z11_2) (bvadd (bvmul c9 z11_3) ?v_21)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z11_0) (bvadd ?v_19 (bvadd (bvmul c0 z11_2) (bvadd (bvmul c6 z11_3) (bvadd (bvneg z11_4) (bvadd ?v_20 (bvadd (bvneg (bvmul c0 z11_4)) (bvadd ?v_21 z11_5)))))))) (_ bv0 6)) (= (bvadd z12_0 (bvadd (bvmul c5 z12_2) (bvadd (bvmul c11 z12_3) (bvneg (bvmul c11 z12_4))))) (_ bv0 6)) (= (bvadd ?v_22 (bvadd (bvmul c2 z12_2) (bvadd (bvmul c8 z12_3) (bvneg (bvmul c8 z12_4))))) (_ bv0 6)) (= (bvadd (bvneg z12_1) (bvadd (bvmul c4 z12_2) (bvadd (bvmul c10 z12_3) (bvneg (bvmul c10 z12_4))))) (_ bv0 6)) (= (bvadd z12_1 (bvadd (bvmul c1 z12_2) (bvadd (bvmul c7 z12_3) ?v_23))) (_ bv0 6)) (= (bvadd (bvmul c3 z12_2) (bvadd (bvmul c9 z12_3) ?v_24)) (_ bv0 6)) (= (bvadd ?v_22 (bvadd z12_1 (bvadd (bvmul c0 z12_2) (bvadd (bvmul c6 z12_3) (bvadd (bvneg z12_4) (bvadd ?v_23 (bvadd (bvneg (bvmul c6 z12_4)) (bvadd ?v_24 z12_5)))))))) (_ bv0 6)) (= (bvadd z13_0 (bvadd (bvmul c5 z13_2) (bvadd (bvmul c11 z13_3) (bvneg (bvmul c5 z13_4))))) (_ bv0 6)) (= (bvadd ?v_25 (bvadd (bvmul c2 z13_2) (bvadd (bvmul c8 z13_3) (bvneg (bvmul c2 z13_4))))) (_ bv0 6)) (= (bvadd (bvneg z13_1) (bvadd (bvmul c4 z13_2) (bvadd (bvmul c10 z13_3) (bvneg (bvmul c4 z13_4))))) (_ bv0 6)) (= (bvadd z13_1 (bvadd (bvmul c1 z13_2) (bvadd (bvmul c7 z13_3) ?v_26))) (_ bv0 6)) (= (bvadd (bvmul c3 z13_2) (bvadd (bvmul c9 z13_3) ?v_27)) (_ bv0 6)) (= (bvadd ?v_25 (bvadd z13_1 (bvadd (bvmul c0 z13_2) (bvadd (bvmul c6 z13_3) (bvadd (bvneg z13_4) (bvadd ?v_26 (bvadd (bvneg (bvmul c0 z13_4)) (bvadd ?v_27 z13_5)))))))) (_ bv0 6)) (= (bvadd z14_0 (bvadd (bvmul c4 z14_2) (bvadd (bvmul c10 z14_3) (bvneg (bvmul c10 z14_4))))) (_ bv0 6)) (= (bvadd (bvneg z14_0) (bvadd (bvmul c1 z14_2) (bvadd (bvmul c7 z14_3) ?v_28))) (_ bv0 6)) (= (bvadd (bvneg z14_1) (bvadd (bvmul c5 z14_2) (bvadd (bvmul c11 z14_3) (bvneg (bvmul c11 z14_4))))) (_ bv0 6)) (= (bvadd z14_1 (bvadd (bvmul c2 z14_2) (bvadd (bvmul c8 z14_3) (bvneg (bvmul c8 z14_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z14_2) (bvadd (bvmul c9 z14_3) ?v_29)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z14_0) (bvadd (bvmul c0 z14_2) (bvadd (bvmul c6 z14_3) (bvadd (bvneg z14_4) (bvadd ?v_28 (bvadd (bvneg (bvmul c6 z14_4)) (bvadd ?v_29 z14_5))))))) (_ bv0 6)) (= (bvadd z15_0 (bvadd (bvmul c4 z15_2) (bvadd (bvmul c10 z15_3) (bvneg (bvmul c4 z15_4))))) (_ bv0 6)) (= (bvadd (bvneg z15_0) (bvadd (bvmul c1 z15_2) (bvadd (bvmul c7 z15_3) ?v_30))) (_ bv0 6)) (= (bvadd (bvneg z15_1) (bvadd (bvmul c5 z15_2) (bvadd (bvmul c11 z15_3) (bvneg (bvmul c5 z15_4))))) (_ bv0 6)) (= (bvadd z15_1 (bvadd (bvmul c2 z15_2) (bvadd (bvmul c8 z15_3) (bvneg (bvmul c2 z15_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z15_2) (bvadd (bvmul c9 z15_3) ?v_31)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z15_0) (bvadd (bvmul c0 z15_2) (bvadd (bvmul c6 z15_3) (bvadd (bvneg z15_4) (bvadd ?v_30 (bvadd (bvneg (bvmul c0 z15_4)) (bvadd ?v_31 z15_5))))))) (_ bv0 6)) (= (bvadd z16_0 (bvadd (bvmul c4 z16_2) (bvadd (bvmul c10 z16_3) (bvneg (bvmul c10 z16_4))))) (_ bv0 6)) (= (bvadd ?v_32 (bvadd (bvmul c1 z16_2) (bvadd (bvmul c7 z16_3) (bvneg (bvmul c7 z16_4))))) (_ bv0 6)) (= (bvadd z16_1 (bvadd (bvmul c5 z16_2) (bvadd (bvmul c11 z16_3) (bvneg (bvmul c11 z16_4))))) (_ bv0 6)) (= (bvadd ?v_33 (bvadd (bvmul c2 z16_2) (bvadd (bvmul c8 z16_3) ?v_34))) (_ bv0 6)) (= (bvadd (bvmul c3 z16_2) (bvadd (bvmul c9 z16_3) ?v_35)) (_ bv0 6)) (= (bvadd ?v_32 (bvadd ?v_33 (bvadd (bvmul c0 z16_2) (bvadd (bvmul c6 z16_3) (bvadd (bvneg z16_4) (bvadd ?v_34 (bvadd (bvneg (bvmul c6 z16_4)) (bvadd ?v_35 z16_5)))))))) (_ bv0 6)) (= (bvadd z17_0 (bvadd (bvmul c4 z17_2) (bvadd (bvmul c10 z17_3) (bvneg (bvmul c4 z17_4))))) (_ bv0 6)) (= (bvadd ?v_36 (bvadd (bvmul c1 z17_2) (bvadd (bvmul c7 z17_3) (bvneg (bvmul c1 z17_4))))) (_ bv0 6)) (= (bvadd z17_1 (bvadd (bvmul c5 z17_2) (bvadd (bvmul c11 z17_3) (bvneg (bvmul c5 z17_4))))) (_ bv0 6)) (= (bvadd ?v_37 (bvadd (bvmul c2 z17_2) (bvadd (bvmul c8 z17_3) ?v_38))) (_ bv0 6)) (= (bvadd (bvmul c3 z17_2) (bvadd (bvmul c9 z17_3) ?v_39)) (_ bv0 6)) (= (bvadd ?v_36 (bvadd ?v_37 (bvadd (bvmul c0 z17_2) (bvadd (bvmul c6 z17_3) (bvadd (bvneg z17_4) (bvadd ?v_38 (bvadd (bvneg (bvmul c0 z17_4)) (bvadd ?v_39 z17_5)))))))) (_ bv0 6)) (= (bvadd z18_0 (bvadd (bvmul c4 z18_2) (bvadd (bvmul c10 z18_3) (bvneg (bvmul c10 z18_4))))) (_ bv0 6)) (= (bvadd ?v_40 (bvadd (bvmul c1 z18_2) (bvadd (bvmul c7 z18_3) (bvneg (bvmul c7 z18_4))))) (_ bv0 6)) (= (bvadd z18_1 (bvadd (bvmul c5 z18_2) (bvadd (bvmul c11 z18_3) (bvneg (bvmul c11 z18_4))))) (_ bv0 6)) (= (bvadd ?v_41 (bvadd (bvmul c2 z18_2) (bvadd (bvmul c8 z18_3) (bvneg (bvmul c8 z18_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z18_2) (bvadd (bvmul c9 z18_3) (bvneg (bvmul c9 z18_4)))) (_ bv0 6)) (= (bvadd ?v_40 (bvadd ?v_41 (bvadd (bvmul c0 z18_2) (bvadd (bvmul c6 z18_3) (bvadd (bvneg z18_4) (bvadd (bvneg (bvmul c6 z18_4)) z18_5)))))) (_ bv0 6)) (= (bvadd z19_0 (bvadd (bvmul c4 z19_2) (bvadd (bvmul c10 z19_3) (bvneg (bvmul c4 z19_4))))) (_ bv0 6)) (= (bvadd ?v_42 (bvadd (bvmul c1 z19_2) (bvadd (bvmul c7 z19_3) (bvneg (bvmul c1 z19_4))))) (_ bv0 6)) (= (bvadd z19_1 (bvadd (bvmul c5 z19_2) (bvadd (bvmul c11 z19_3) (bvneg (bvmul c5 z19_4))))) (_ bv0 6)) (= (bvadd ?v_43 (bvadd (bvmul c2 z19_2) (bvadd (bvmul c8 z19_3) (bvneg (bvmul c2 z19_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z19_2) (bvadd (bvmul c9 z19_3) (bvneg (bvmul c3 z19_4)))) (_ bv0 6)) (= (bvadd ?v_42 (bvadd ?v_43 (bvadd (bvmul c0 z19_2) (bvadd (bvmul c6 z19_3) (bvadd (bvneg z19_4) (bvadd (bvneg (bvmul c0 z19_4)) z19_5)))))) (_ bv0 6)) (= (bvadd z20_0 (bvadd (bvmul c4 z20_2) (bvadd (bvmul c10 z20_3) (bvneg (bvmul c10 z20_4))))) (_ bv0 6)) (= (bvadd ?v_44 (bvadd (bvmul c1 z20_2) (bvadd (bvmul c7 z20_3) (bvneg (bvmul c7 z20_4))))) (_ bv0 6)) (= (bvadd (bvneg z20_1) (bvadd (bvmul c5 z20_2) (bvadd (bvmul c11 z20_3) (bvneg (bvmul c11 z20_4))))) (_ bv0 6)) (= (bvadd z20_1 (bvadd (bvmul c2 z20_2) (bvadd (bvmul c8 z20_3) (bvneg (bvmul c8 z20_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z20_2) (bvadd (bvmul c9 z20_3) (bvneg (bvmul c9 z20_4)))) (_ bv0 6)) (= (bvadd ?v_44 (bvadd (bvmul c0 z20_2) (bvadd (bvmul c6 z20_3) (bvadd (bvneg z20_4) (bvadd (bvneg (bvmul c6 z20_4)) z20_5))))) (_ bv0 6)) (= (bvadd z21_0 (bvadd (bvmul c4 z21_2) (bvadd (bvmul c10 z21_3) (bvneg (bvmul c4 z21_4))))) (_ bv0 6)) (= (bvadd ?v_45 (bvadd (bvmul c1 z21_2) (bvadd (bvmul c7 z21_3) (bvneg (bvmul c1 z21_4))))) (_ bv0 6)) (= (bvadd (bvneg z21_1) (bvadd (bvmul c5 z21_2) (bvadd (bvmul c11 z21_3) (bvneg (bvmul c5 z21_4))))) (_ bv0 6)) (= (bvadd z21_1 (bvadd (bvmul c2 z21_2) (bvadd (bvmul c8 z21_3) (bvneg (bvmul c2 z21_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z21_2) (bvadd (bvmul c9 z21_3) (bvneg (bvmul c3 z21_4)))) (_ bv0 6)) (= (bvadd ?v_45 (bvadd (bvmul c0 z21_2) (bvadd (bvmul c6 z21_3) (bvadd (bvneg z21_4) (bvadd (bvneg (bvmul c0 z21_4)) z21_5))))) (_ bv0 6)) (= (bvadd z22_0 (bvadd (bvmul c5 z22_2) (bvadd (bvmul c11 z22_3) (bvneg (bvmul c11 z22_4))))) (_ bv0 6)) (= (bvadd (bvneg z22_0) (bvadd (bvmul c2 z22_2) (bvadd (bvmul c8 z22_3) ?v_46))) (_ bv0 6)) (= (bvadd (bvneg z22_1) (bvadd (bvmul c4 z22_2) (bvadd (bvmul c10 z22_3) (bvneg (bvmul c10 z22_4))))) (_ bv0 6)) (= (bvadd z22_1 (bvadd (bvmul c1 z22_2) (bvadd (bvmul c7 z22_3) (bvneg (bvmul c7 z22_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z22_2) (bvadd (bvmul c9 z22_3) ?v_47)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z22_0) (bvadd (bvmul c0 z22_2) (bvadd (bvmul c6 z22_3) (bvadd (bvneg z22_4) (bvadd ?v_46 (bvadd (bvneg (bvmul c6 z22_4)) (bvadd ?v_47 z22_5))))))) (_ bv0 6)) (= (bvadd z23_0 (bvadd (bvmul c5 z23_2) (bvadd (bvmul c11 z23_3) (bvneg (bvmul c5 z23_4))))) (_ bv0 6)) (= (bvadd (bvneg z23_0) (bvadd (bvmul c2 z23_2) (bvadd (bvmul c8 z23_3) ?v_48))) (_ bv0 6)) (= (bvadd (bvneg z23_1) (bvadd (bvmul c4 z23_2) (bvadd (bvmul c10 z23_3) (bvneg (bvmul c4 z23_4))))) (_ bv0 6)) (= (bvadd z23_1 (bvadd (bvmul c1 z23_2) (bvadd (bvmul c7 z23_3) (bvneg (bvmul c1 z23_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z23_2) (bvadd (bvmul c9 z23_3) ?v_49)) (_ bv0 6)) (= (bvadd (bvmul (_ bv62 6) z23_0) (bvadd (bvmul c0 z23_2) (bvadd (bvmul c6 z23_3) (bvadd (bvneg z23_4) (bvadd ?v_48 (bvadd (bvneg (bvmul c0 z23_4)) (bvadd ?v_49 z23_5))))))) (_ bv0 6)) (= (bvadd z24_0 (bvadd (bvmul c5 z24_2) (bvadd (bvmul c11 z24_3) (bvneg (bvmul c11 z24_4))))) (_ bv0 6)) (= (bvadd ?v_50 (bvadd (bvmul c2 z24_2) (bvadd (bvmul c8 z24_3) (bvneg (bvmul c8 z24_4))))) (_ bv0 6)) (= (bvadd (bvneg z24_1) (bvadd (bvmul c4 z24_2) (bvadd (bvmul c10 z24_3) (bvneg (bvmul c10 z24_4))))) (_ bv0 6)) (= (bvadd z24_1 (bvadd (bvmul c1 z24_2) (bvadd (bvmul c7 z24_3) (bvneg (bvmul c7 z24_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z24_2) (bvadd (bvmul c9 z24_3) (bvneg (bvmul c9 z24_4)))) (_ bv0 6)) (= (bvadd ?v_50 (bvadd (bvmul c0 z24_2) (bvadd (bvmul c6 z24_3) (bvadd (bvneg z24_4) (bvadd (bvneg (bvmul c6 z24_4)) z24_5))))) (_ bv0 6)) (= (bvadd z25_0 (bvadd (bvmul c5 z25_2) (bvadd (bvmul c11 z25_3) (bvneg (bvmul c5 z25_4))))) (_ bv0 6)) (= (bvadd ?v_51 (bvadd (bvmul c2 z25_2) (bvadd (bvmul c8 z25_3) (bvneg (bvmul c2 z25_4))))) (_ bv0 6)) (= (bvadd (bvneg z25_1) (bvadd (bvmul c4 z25_2) (bvadd (bvmul c10 z25_3) (bvneg (bvmul c4 z25_4))))) (_ bv0 6)) (= (bvadd z25_1 (bvadd (bvmul c1 z25_2) (bvadd (bvmul c7 z25_3) (bvneg (bvmul c1 z25_4))))) (_ bv0 6)) (= (bvadd (bvmul c3 z25_2) (bvadd (bvmul c9 z25_3) (bvneg (bvmul c3 z25_4)))) (_ bv0 6)) (= (bvadd ?v_51 (bvadd (bvmul c0 z25_2) (bvadd (bvmul c6 z25_3) (bvadd (bvneg z25_4) (bvadd (bvneg (bvmul c0 z25_4)) z25_5))))) (_ bv0 6)))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
